%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                           %
% SELLF specification for LJ with           %
% additive and multiplicative connectives   %
%                                           %
% Giselle Reis   -   2015                   %
%                                           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% The sequents will be Gamma |- Delta 
% where Gamma and Delta are multi-sets of formulas (linear)
% and Delta contains at most one formuls at all times.
% The fact that sometimes the context is copied and sometimes 
% it is split is encoded in the rules themselves.

subexp r lin.
subexp l lin.

subexpctx r single rght.
subexpctx l many lft.

rules introduction.

% Implication
(not (lft (imp A B))) *  (([l]bang ([r]? (rght A))) * ([l]? (lft B))).
(not (rght (imp A B))) *  (([l]? (lft A)) | ([r]? (rght B))).

% Disjunction
(not (lft (or A B))) * (([l]? (lft A)) & ([l]? (lft B))).
(not (rght (or A B))) * (([r]? (rght A)) + ([r]? (rght B))).

% Conjunction additive
(not (lft (andA A B))) * (([l]? (lft A)) + ([l]? (lft B))).
(not (rght (andA A B))) * (([r]? (rght A)) & ([r]? (rght B))).

% Conjunction multiplicative
(not (lft (andM A B))) * (([l]? (lft A)) | ([l]? (lft B))).
(not (rght (andM A B))) * (([r]? (rght A)) * ([r]? (rght B))).

rules axiom.
((not (lft A)) * (not (rght A))).

